In this paper, we develop compositional methods for formally verifyingdifferential privacy for algorithms whose analysis goes beyond the compositiontheorem. Our methods are based on the observation that differential privacy hasdeep connections with a generalization of probabilistic couplings, anestablished mathematical tool for reasoning about stochastic processes. Evenwhen the composition theorem is not helpful, we can often prove privacy by acoupling argument. We demonstrate our methods on two algorithms: the Exponential mechanism andthe Above Threshold algorithm, the critical component of the famous SparseVector algorithm. We verify these examples in a relational program logicapRHL+, which can construct approximate couplings. This logic extends theexisting apRHL logic with more general rules for the Laplace mechanism and theone-sided Laplace mechanism, and new structural rules enabling pointwisereasoning about privacy; all the rules are inspired by the connection withcoupling. While our paper is presented from a formal verification perspective,we believe that its main insight is of independent interest for thedifferential privacy community.
展开▼
